COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00010 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.ONCE center
%6ON THE MODEL THEORY OF KNOWLEDGE%1
.SKIP 2
The need to represent information about who knows what in intelligent computer
programs was the original motivation for this work.  For example, a program
that arranges trips must know that travel agents know who knows the availability of 
rooms in hotels.  An early problem is how to represent what people know
about other people's knowledge of facts, and even the knowledge of propositions
treated in this paper presented some problems that were not treated in
previous literature.

We started with the following well known puzzle of the three wise men: %2
A king wishing to know which of his three wise men is the wisest, paints a
white spot on each of their foreheads, tells them at least one spot is
white, and asks each to determine the color of his spot.  After a while the
smartest announces that his spot is white reasoning as follows:  "Suppose
my spot were black.  The second wisest of us would then see a black and
a white and would reason that if his spot were black, the dumbest would
see two black spots and would conclude that his spot is white on the basis
of the king's assurance.  He would have announced it by now, so my spot
must be white."%1

In formalizing the puzzle, we don't wish to try to formalize reasoning about
how fast other people reason.  Therefore, we will imagine that either the
king asks the wise men in sequence whether they know the colors of their
spots or that he asks synchronously, "Do you know the color of your spot"
getting a chorus of noes.  He asks it again with the same result, but on
the third asking, they answer that their spots are white.  Needless to say,
we are also not formalizing any notion of relative wisdom.

We start with a general set of axioms for knowledge based on the notation, axioms,
and inference rules of propositional calculus supplemented by the notation
%2S*p%1 standing for, "Person S knows proposition p."  Thus %2W3*W2%8j%2(W1*p1)%1
can stand for, "The third wise man knows that the second wise man knows that the first
wise man does not know that the first wise man's spot is white".

We use axiom achemata with subscripted S's as person variables, subscripted p's and
q's as propositional variables, and a special person constant called "any fool"
and denoted by 0.  It is convenient to introduce "any fool" because whatever
he knows, every one knows everyone else knows.  "Any fool" is especially
useful when an event occurs in front of all the knowers, and we need a sentence
like, "S1 knows that S2 knows that S3 knows etc.".  Here are the schemata:

.begin indent 0,5; turn on "\";
K0:\S*p ⊃ p; What a person knows is true.

K1:\0*(S*p ⊃ p); Any fool knows that what a person knows is true.

K2:\0*(0*p ⊃ 0*S*p); What any fool knows, any fool knows everyone knows, and
and any fool knows that.

K3:\0*(S*p ∧ S*(p ⊃ q) ⊃ S*q); Any fool knows everyone can do modus ponens.

There are two optional schemata K4 and K5:

K4:\0*(S*p ⊃ S*S*p); Any fool knows that what someone knows, he knows he knows.

K5:\0*(%8j%*S*p ⊃ S*%8j%*S*p); Any fool knows that what someone doesn't know
he knows he doesn't know.
.end

If there is only one person S, the system is equivalent to a system of modal
logic.  Axioms K0-K3 give a system equivalent to what Hughes and Cresswell[1]
call T, and K4 and K5 give the modal systems S4 and S5 respectively.  We
call K4 and K5 the introspective schemata.  It is convenient to write 
S$p as an abbreviation for S*p ∨ S* %8j%* p; it may be read, "S knows whether
p".

On the basis of these schemata we may axiomatize the wise man problem as
follows:

.begin nofill;
C0:  p1 ∧ p2 ∧ p3
C1:  0*(p1 ∨ p2 ∨ p3)
C2:  0*(S1α$p2 ∧ S1α$p3 ∧ S2α$p1 ∧ S2α$p3 ∧ S3α$p1 ∧ S3α$p2)
C3:  0*(S2α$S1-p1)
C4:  0*(S3α$S2*p2)
C5:  %8j%*S1α$p1
C6:  %8j%*S2α$p2
.end

From K0-K3 and C1-C6 it is possible to prove S3*p3.  C0 is not used in the proof. 
In some sense C5 and C6 should not be required.  Looking at the problem
sequentially, it should follow that S1 does not know p1 initially, an that
even knowing that, S2 doesn't know p2.

In order to proceed further with the problem, model theoretic semantics is
necessary.  The semantics we give is a generalization of that for modal logics
due to Kripke.  Using the completeness result of our systems for
Kripke-type semantics, we have given a model theoretic solution of the puzzle.

We also deal with formal analysis of the puzzle of unfaithful wives along
the same line, but it requires to treat the notion of time as well.  The
reader is referred to Sato[2] for details.
.skip
.once center
%6References%1
.skip
.begin indent 0,5; turn on "\";
[1]\Hughes, G.E., and Cresswell, M.J., %3An Introduction to Modal Logic%*,
London: Methuen and Co., 1968.

[2]\Sato, M., %2A study of Kripke-type models for some modal logics by
Gentzen's sequential method%*, Technical Report RIMS-206, RIMS, Kyoto
University 1976, to appear in Publ. RIMS, Vol. 13, No. 2, 1977.
.end